First of all, you can give a name for your model using the following syntax in the first line of your model. The model name is used internally as an ID for simulator to find the correct drawing pictures, if any. It is optional.

//@@Model Name@@

Constants

Variables/arrays

A global variable is defined using the following syntax,

var knight = 0;

wherevar is a key word for defining a variable and knight is the variable name. Initially, knight has the value 0. Semi-colon is used to mark the end of the 'sentence' as above. We remark the input language of PAT is weakly typed and therefore no typing information is required when declaring a variable. Cast between incompatible types may result in a run-time exception.

A fixed-size array may be defined as follows,

var board = [3, 5, 6, 0, 2, 7, 8, 4, 1];

where board is the array name and its initial value is specified as the sequence, e.g., board[0] = 3. The following defines an array of size 3.

var leader[3];

All elements in the array are initialized to be 0.

Note for multi-dimensional array: PAT supports multi-dimensional arrays by converting them into one dimensional arrays. You can declare and use multi-dimensional arrays as follows (Note that here, the N should be a constant). The only restriction is that you can not assign multi-dimensional array constant to multi-dimensional arrays variables. To initialize a multi-dimensional array, you need to do it explicitly in some events.

• var matrix[3*N][10];

Note: To assign values to specific elements in an array, you can use event prefix. For example:

 P() = a { matrix[1][9] = 0 } -> Skip;

Variable range specification: users can provide the range of the variables/arrays explicitly by giving lower bound or upper bound or both. In this way, the model checkers and simulator can report the out-of-range violation of the variable values to help users to monitor the variable values. The syntax of specifying range values are demonstrated as follows.

• var knight : {0..} = 0;
• var board : {0..10} = [3, 5, 6, 0, 2, 7, 8, 4, 1];
• var leader[N] : {..N-1}; //where N is a constant defined.

Array Initialization: To ease the modeling, PAT supports fast array initialization using following syntax.

• #define N 2;
• var array = [1(2), 3..6, 7(N*2), 12..10];
• //the above is same as the following
• var array = [1, 1, 3, 4, 5, 6, 7, 7, 7, 7, 12, 11, 10];

In the above syntax, 1(2) and 7(N*2) allow user to quickly create an array with same initial values. 3..6 and 12..10 allow user to write quick increasing and decreasing loop to initialize the array.

User defined type: To ease the modeling, PAT allows users to define any data structures and use them in PAT models. The following shows the syntax.

• var<Type> x ; //default constructor of Type class will be called.
• var<Type> x = new Type(1, 2); //constructor with two int parameters will be called.

Hidden variable: To simplify the model, PAT introduces the hidden variables which can be used as normal variables. The only difference is that hidden variable is a kind of secondary variable, which is not included in the state details. The idea of secondary is to use redundant variable to make the modeling easier.

• var a; var b;
• hvar difference; //secondary variable to store the difference between a and b.

Note: It is user's responsibility to make sure that hidden variables don't introduce any new states. If you not sure about this, you can change hvar to var to see any difference in terms of states in the simulation or verification.

Channels

wherechannel is a key word for declaring channels only, c is the channel name and 5 is the channel buffer size; Channel buffer size must be greater or equal to 0. Notice that a channel with buffer size 0 sends/receives messages synchronously. This is used to model pair-wise synchronization, which involves two parties. Barrier-synchronization, which involves multiple parties, is supported by following CSP's approach, i.e., alphabetized parallel composition.  

Note: Currently, channel array is also supported.

           channel c[4] 5;

Macro

In addition, the key word #define may be used to define macro. For instance,

#define goal x == 0;

where goal is the name of the macro and x == 0 is what goal means. A macro name is used in the same way as global constant is used. For instance, given the above definition, we may write the following,

if (goal) { P } else { Q };

which means if the value of x is 0 then do P else do Q. We remark that macro can be used in LTL formulae.

Furthermore, macro can take in parameters as defined below. When calling the macro, the keyword call is used. The macro expression can be any possible expression in PAT (if, local variable declarition, while, assignment).

#define multi(i,j) i*j;

System  = if (call(multi, 3,4) >12 ) { a -> Skip } else { b -> Skip };

Model Inclusion

If the model is too big, you can split the model to several files and include them in the main model by using the include keyword. For example,

#include "c:\example.csp";

If the model is in the same folder of the main model, you can only put the file name. Note that: Nested inclusion in files are also possible in PAT, and duplicated inclusion will be ignored.

To open the included file, you can select the file path, then right click the button and choose "open import/include file" function to open it. This funcation can recognize both absolute path and relative path to the current model file. The picture below shows how to open an included file.